NEXT ·  UP ·  PREVIOUS ·  CONTENTS ·  INDEX
Next:Proof: Up:Induction for lists Previous:Induction for lists

Proof:

The proof is by induction on l$\sb{\hbox{\scriptsize 1}}$.The initial step is to show that this proposition holds when l$\sb{\hbox{\scriptsize 1}}$ is the empty list, []. Using properties of the append operator, we conclude rev() = revl$\sb{\hbox{\scriptsize 2}}$ = = as required.

Now assume rev () = and consider h :: t.

LHS = rev()  
  = rev()     [defn of @]
  =     [defn of rev]
  =     [induction hypothesis]
  =     [defn of rev]
  = RHS  
$\Box$

Exercise

Prove by structural induction that for all 'a lists l$\sb{\hbox{\scriptsize 1}}$ and l$\sb{\hbox{\scriptsize 2}}$

length () = length l$\sb{\hbox{\scriptsize 1}}$+ length l$\sb{\hbox{\scriptsize 2}}$.

Proposition (Involution)

The rev function is an involution, i.e. it always undoes its own work, since rev(revl) = l.

NEXT ·  UP ·  PREVIOUS ·  CONTENTS ·  INDEX
Next:Proof: Up:Induction for lists Previous:Induction for lists